<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>GMFFExporter</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="GMFFExporter";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/GMFFExporterTypesetDefs.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/GMFFExporter.html" target="_top">Frames</a></li>
<li><a href="GMFFExporter.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.gmff</div>
<h2 title="Class GMFFExporter" class="title">Class GMFFExporter</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.gmff.GMFFExporter</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>Direct Known Subclasses:</dt>
<dd><a href="../../mmj/gmff/ModelAExporter.html" title="class in mmj.gmff">ModelAExporter</a></dd>
</dl>
<hr>
<br>
<pre>public abstract class <span class="strong">GMFFExporter</span>
extends java.lang.Object</pre>
<div class="block"><code>GMFFExporter</code> is the base class for creating export files.
 <p>
 There can be multiple Exporters in use at one time but the key is Export Type
 (e.g. "html", "althtml", etc.) and only one Exporter of a given Export Type
 can be active at one time.
 <p>
 The Export Type key is used to bring together and consolidate the various
 RunParm settings at GMFF initialization time.
 <p>
 What this all boils down to is that there cannot be two different Models in
 use for, say, Export Type "html" in a single execution of mmj2. However, the
 Export Type code is arbitrary and no functionality is hard-coded based on
 Export Type. So it is possible to define another Export Type such as "html2"
 which and use say, Model B, at the same time that Export Type "html" uses
 Model A -- you would just need to define all of the relevant parameters,
 including the Export Directory (so that the two exports don't overwrite each
 other.)
 <p>
 <code>GMFFExporter</code> also contains a Map holding a cache of Model Files --
 <code>modelFileCacheMap</code> for the given Export Type. The purpose is to avoid
 re-reading the model files over and over again.
 <p>
 <code>GMFFExporter</code> also contains a number of utility functions which are
 common to the different model exporters, such as <code>ModelAExporter</code>,
 which is an extension of <code>GMFFExporter</code>.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#GMFFExporter(mmj.gmff.GMFFManager, mmj.gmff.GMFFExportParms, mmj.gmff.GMFFUserTextEscapes)">GMFFExporter</a></strong>(<a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a>&nbsp;gmffManager,
            <a href="../../mmj/gmff/GMFFExportParms.html" title="class in mmj.gmff">GMFFExportParms</a>&nbsp;gmffExportParms,
            <a href="../../mmj/gmff/GMFFUserTextEscapes.html" title="class in mmj.gmff">GMFFUserTextEscapes</a>&nbsp;gmffUserTextEscapes)</code>&nbsp;</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#appendMandatoryModelFile(java.lang.StringBuilder, java.lang.String, java.lang.String)">appendMandatoryModelFile</a></strong>(java.lang.StringBuilder&nbsp;exportBuffer,
                        java.lang.String&nbsp;mandatoryModelFileName,
                        java.lang.String&nbsp;theoremLabel)</code>
<div class="block">Outputs the contents of a Mandatory Model File to the export buffer
 throwing an exception if the file is not found.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#appendModelFileText(java.lang.StringBuilder, java.lang.String)">appendModelFileText</a></strong>(java.lang.StringBuilder&nbsp;exportBuffer,
                   java.lang.String&nbsp;modelFileText)</code>
<div class="block">Appends text from a Model File to the output StringBuilder.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static <a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#ConstructModelExporter(mmj.gmff.GMFFManager, mmj.gmff.GMFFExportParms, mmj.gmff.GMFFUserTextEscapes)">ConstructModelExporter</a></strong>(<a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a>&nbsp;gmffManager,
                      <a href="../../mmj/gmff/GMFFExportParms.html" title="class in mmj.gmff">GMFFExportParms</a>&nbsp;gmffExportParms,
                      <a href="../../mmj/gmff/GMFFUserTextEscapes.html" title="class in mmj.gmff">GMFFUserTextEscapes</a>&nbsp;gmffUserTextEscapes)</code>
<div class="block">A factory for generating GMFFExporters according to Model Id.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#escapeAndAppendProofText(java.lang.StringBuilder, java.lang.String)">escapeAndAppendProofText</a></strong>(java.lang.StringBuilder&nbsp;exportBuffer,
                        java.lang.String&nbsp;proofText)</code>
<div class="block">Appends non-typeset text to the output buffer after escaping the text.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>abstract java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#exportProofWorksheet(mmj.gmff.ProofWorksheetCache, java.lang.String)">exportProofWorksheet</a></strong>(<a href="../../mmj/gmff/ProofWorksheetCache.html" title="class in mmj.gmff">ProofWorksheetCache</a>&nbsp;proofWorksheetCache,
                    java.lang.String&nbsp;appendFileName)</code>
<div class="block">Abstract method to export a Proof Worksheet according to the pattern of a
 Model.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#getMandatoryModelFile(java.lang.String, java.lang.String)">getMandatoryModelFile</a></strong>(java.lang.String&nbsp;mandatoryModelFileName,
                     java.lang.String&nbsp;theoremLabel)</code>
<div class="block">Returns a String containing the contents of a mandatory Model File.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#getMessages()">getMessages</a></strong>()</code>
<div class="block">Get function to return the <code>Messages</code> object.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#getOptionalModelFile(java.lang.String)">getOptionalModelFile</a></strong>(java.lang.String&nbsp;optionalModelFileName)</code>
<div class="block">Returns a String containing the contents of an optional Model File.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#loadMinProofWorksheet(mmj.gmff.ProofWorksheetCache)">loadMinProofWorksheet</a></strong>(<a href="../../mmj/gmff/ProofWorksheetCache.html" title="class in mmj.gmff">ProofWorksheetCache</a>&nbsp;p)</code>
<div class="block">Loads a <code>MinProofWorksheet</code> object using the cached
 <code>proofText</code> if the cache does not already contain a loaded instance
 of the <code>MinProofWorksheet</code>.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#outputToExportFile(java.lang.StringBuilder, java.lang.String, java.lang.String)">outputToExportFile</a></strong>(java.lang.StringBuilder&nbsp;exportText,
                  java.lang.String&nbsp;appendFileName,
                  java.lang.String&nbsp;theoremLabel)</code>
<div class="block">Writes the exported text to an output file.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#readModelFile(java.lang.String)">readModelFile</a></strong>(java.lang.String&nbsp;modelFileName)</code>
<div class="block">Returns the cached model file contents or if not cached already reads the
 model file from disk and caches it.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#typesetAndAppendToken(java.lang.StringBuilder, java.lang.String, java.lang.String)">typesetAndAppendToken</a></strong>(java.lang.StringBuilder&nbsp;exportBuffer,
                     java.lang.String&nbsp;token,
                     java.lang.String&nbsp;theoremLabel)</code>
<div class="block">If possible typesets the input token and outputs to the buffer.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFExporter.html#writeExportFile(java.lang.String, java.lang.StringBuilder, boolean)">writeExportFile</a></strong>(java.lang.String&nbsp;exportFileName,
               java.lang.StringBuilder&nbsp;exportBuffer,
               boolean&nbsp;append)</code>
<div class="block">Writes the export text to the specified file and returns a String
 containing the absolute path of the output file.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="GMFFExporter(mmj.gmff.GMFFManager, mmj.gmff.GMFFExportParms, mmj.gmff.GMFFUserTextEscapes)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>GMFFExporter</h4>
<pre>public&nbsp;GMFFExporter(<a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a>&nbsp;gmffManager,
            <a href="../../mmj/gmff/GMFFExportParms.html" title="class in mmj.gmff">GMFFExportParms</a>&nbsp;gmffExportParms,
            <a href="../../mmj/gmff/GMFFUserTextEscapes.html" title="class in mmj.gmff">GMFFUserTextEscapes</a>&nbsp;gmffUserTextEscapes)</pre>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="ConstructModelExporter(mmj.gmff.GMFFManager, mmj.gmff.GMFFExportParms, mmj.gmff.GMFFUserTextEscapes)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ConstructModelExporter</h4>
<pre>public static&nbsp;<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;ConstructModelExporter(<a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a>&nbsp;gmffManager,
                                  <a href="../../mmj/gmff/GMFFExportParms.html" title="class in mmj.gmff">GMFFExportParms</a>&nbsp;gmffExportParms,
                                  <a href="../../mmj/gmff/GMFFUserTextEscapes.html" title="class in mmj.gmff">GMFFUserTextEscapes</a>&nbsp;gmffUserTextEscapes)
                                           throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">A factory for generating GMFFExporters according to Model Id.
 <p>
 Right now only Model A is defined, so this code looks peculiar.
 <p>
 Note: The Exporter's <code>gmffExporterTypesetDefs</code> are loaded at
 GMFFInitialize time, and are left null when the Exporter is initially
 constructed.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>gmffManager</code> - The <code>GMFFManager</code> instance.</dd><dd><code>gmffExportParms</code> - Export Parms for the output <code>GMFFExporter</code></dd><dd><code>gmffUserTextEscapes</code> - Text Escapes for the output
            <code>GMFFExporter</code></dd>
<dt><span class="strong">Returns:</span></dt><dd>the newly created <code>GMFFExporter</code></dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="exportProofWorksheet(mmj.gmff.ProofWorksheetCache, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportProofWorksheet</h4>
<pre>public abstract&nbsp;java.lang.String&nbsp;exportProofWorksheet(<a href="../../mmj/gmff/ProofWorksheetCache.html" title="class in mmj.gmff">ProofWorksheetCache</a>&nbsp;proofWorksheetCache,
                                    java.lang.String&nbsp;appendFileName)</pre>
<div class="block">Abstract method to export a Proof Worksheet according to the pattern of a
 Model.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofWorksheetCache</code> - <code>ProofWorksheetCache</code> object containing
            the proof to be exported.</dd><dd><code>appendFileName</code> - File Name (minus File Type) of append file if the
            regular file name is to be overridden (see documentation of
            appendFileNames in GMFFDoc\GMFFRunParms.txt).</dd>
<dt><span class="strong">Returns:</span></dt><dd>Confirmation message of the successful export showing the
         absolute path of the output file -- or <code>null</code> if the export
         failed (error messages are accumed in the <code>Messages</code>
         object.)</dd></dl>
</li>
</ul>
<a name="getMessages()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMessages</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;getMessages()</pre>
<div class="block">Get function to return the <code>Messages</code> object.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>the <code>Messages</code> object.</dd></dl>
</li>
</ul>
<a name="appendMandatoryModelFile(java.lang.StringBuilder, java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>appendMandatoryModelFile</h4>
<pre>public&nbsp;void&nbsp;appendMandatoryModelFile(java.lang.StringBuilder&nbsp;exportBuffer,
                            java.lang.String&nbsp;mandatoryModelFileName,
                            java.lang.String&nbsp;theoremLabel)
                              throws <a href="../../mmj/gmff/GMFFMandatoryModelNotFoundException.html" title="class in mmj.gmff">GMFFMandatoryModelNotFoundException</a>,
                                     <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Outputs the contents of a Mandatory Model File to the export buffer
 throwing an exception if the file is not found.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exportBuffer</code> - <code>StringBuilder</code> containing the contents of the
            export file.</dd><dd><code>mandatoryModelFileName</code> - the File Name of the Model File within the
            Models Directory for this Export Type.</dd><dd><code>theoremLabel</code> - provided for use in error messages.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFMandatoryModelNotFoundException.html" title="class in mmj.gmff">GMFFMandatoryModelNotFoundException</a></code> - if the Model File is not
             found.</dd>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if other errors encountered (such as I/O errors.)</dd></dl>
</li>
</ul>
<a name="appendModelFileText(java.lang.StringBuilder, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>appendModelFileText</h4>
<pre>public&nbsp;void&nbsp;appendModelFileText(java.lang.StringBuilder&nbsp;exportBuffer,
                       java.lang.String&nbsp;modelFileText)</pre>
<div class="block">Appends text from a Model File to the output StringBuilder.
 <p>
 NOTE: does not escape the text because it is from a Model File and should
 already be escaped (as needed.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exportBuffer</code> - <code>StringBuilder</code> containing the contents of the
            export file.</dd><dd><code>modelFileText</code> - data from the Model File to be appended to the
            exportBuffer.</dd></dl>
</li>
</ul>
<a name="typesetAndAppendToken(java.lang.StringBuilder, java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>typesetAndAppendToken</h4>
<pre>public&nbsp;void&nbsp;typesetAndAppendToken(java.lang.StringBuilder&nbsp;exportBuffer,
                         java.lang.String&nbsp;token,
                         java.lang.String&nbsp;theoremLabel)</pre>
<div class="block">If possible typesets the input token and outputs to the buffer.
 <p>
 <ul>
 if token found in typesetting table, appends the replacement text from
 the table to the export buffer -- and returns. Otherwise...
 <li>if not found in the typesetting table then escapes it as text and
 appends it,
 <li>if the not-found token is a valid, non-WorkVar symbol then an error
 message is sent about the missing typesetting table entry.
 </ul>
 <p>
 Note: In the situation where the image file (.gif) referenced by the
 typesetting replacement text is not present in the Export Directory, some
 browsers display "ALT=" text. The Metamath set.mm $t statement uses the
 "ALT=" feature to display the ASCII token text. So in this scenario it
 may appear that the token was not found in the typesetting table, but the
 absence of an error message indicates that that is not the case.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exportBuffer</code> - <code>StringBuilder</code> containing the contents of the
            export file.</dd><dd><code>token</code> - the Metamath token to be typeset.</dd><dd><code>theoremLabel</code> - provided for use in error messages.</dd></dl>
</li>
</ul>
<a name="escapeAndAppendProofText(java.lang.StringBuilder, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>escapeAndAppendProofText</h4>
<pre>public&nbsp;void&nbsp;escapeAndAppendProofText(java.lang.StringBuilder&nbsp;exportBuffer,
                            java.lang.String&nbsp;proofText)</pre>
<div class="block">Appends non-typeset text to the output buffer after escaping the text.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exportBuffer</code> - <code>StringBuilder</code> containing the contents of the
            export file.</dd><dd><code>proofText</code> - output text from the proof worksheet to be escaped and
            appended to the output buffer.</dd></dl>
</li>
</ul>
<a name="getMandatoryModelFile(java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandatoryModelFile</h4>
<pre>public&nbsp;java.lang.String&nbsp;getMandatoryModelFile(java.lang.String&nbsp;mandatoryModelFileName,
                                     java.lang.String&nbsp;theoremLabel)
                                       throws <a href="../../mmj/gmff/GMFFMandatoryModelNotFoundException.html" title="class in mmj.gmff">GMFFMandatoryModelNotFoundException</a>,
                                              <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Returns a String containing the contents of a mandatory Model File.
 <p>
 Invokes the routine to read the Model File from the cache and if not
 found -- because it is a Mandatory Model File -- throws the
 <code>GMFFMandatoryModelNotFoundException</code> exception.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mandatoryModelFileName</code> - the File Name of the Model File within the
            Models Directory for this Export Type.</dd><dd><code>theoremLabel</code> - provided for use in error messages.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String containing the contents of the Model File.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFMandatoryModelNotFoundException.html" title="class in mmj.gmff">GMFFMandatoryModelNotFoundException</a></code> - if the Model File is not
             found.</dd>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if other errors encountered (such as I/O errors.)</dd></dl>
</li>
</ul>
<a name="getOptionalModelFile(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getOptionalModelFile</h4>
<pre>public&nbsp;java.lang.String&nbsp;getOptionalModelFile(java.lang.String&nbsp;optionalModelFileName)
                                      throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Returns a String containing the contents of an optional Model File.
 <p>
 Invokes the routine to read the Model File from the cache and if not
 found -- because it is an Optional Model File -- simply returns
 <code>null</code>.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>optionalModelFileName</code> - the File Name of the Model File within the
            Models Directory for this Export Type.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String containing the contents of the Model File.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="readModelFile(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>readModelFile</h4>
<pre>public&nbsp;java.lang.String&nbsp;readModelFile(java.lang.String&nbsp;modelFileName)
                               throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a>,
                                      <a href="../../mmj/gmff/GMFFFileNotFoundException.html" title="class in mmj.gmff">GMFFFileNotFoundException</a></pre>
<div class="block">Returns the cached model file contents or if not cached already reads the
 model file from disk and caches it.
 <p>
 Returns the file contents as a String, or throws an exception if not
 found.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>modelFileName</code> - the File Name of the Model File within the Models
            Directory for this Export Type.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String containing the contents of the Model File.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFFileNotFoundException.html" title="class in mmj.gmff">GMFFFileNotFoundException</a></code> - if the Model File is not found.</dd>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if other errors encountered (such as I/O errors.)</dd></dl>
</li>
</ul>
<a name="loadMinProofWorksheet(mmj.gmff.ProofWorksheetCache)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>loadMinProofWorksheet</h4>
<pre>protected&nbsp;void&nbsp;loadMinProofWorksheet(<a href="../../mmj/gmff/ProofWorksheetCache.html" title="class in mmj.gmff">ProofWorksheetCache</a>&nbsp;p)
                              throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Loads a <code>MinProofWorksheet</code> object using the cached
 <code>proofText</code> if the cache does not already contain a loaded instance
 of the <code>MinProofWorksheet</code>.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>p</code> - the ProofWorksheetCache object.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="outputToExportFile(java.lang.StringBuilder, java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>outputToExportFile</h4>
<pre>protected&nbsp;java.lang.String&nbsp;outputToExportFile(java.lang.StringBuilder&nbsp;exportText,
                                  java.lang.String&nbsp;appendFileName,
                                  java.lang.String&nbsp;theoremLabel)
                                       throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Writes the exported text to an output file.
 <p>
 Note: the name of the output file is generated here and it is a bit
 tricky. There is a hierarchy of possibilities:
 <ul>
 <li>if <code>appendFileName</code> is not null then that is the name used, and
 the file is opened in "append mode", meaning the output is written to the
 end of the file if the file already exists.
 <li>otherwise, if the Export Parms specify an output file name then that
 is the name used.
 <li>otherwise, the <code>theoremLabel</code> is used as the file name.
 </ul>
 <p>
 Finally, to note, the output file name's File Type is appended to the
 file name computed above, in every case.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exportText</code> - the contents to be written out.</dd><dd><code>appendFileName</code> - File Name (minus File Type) of append file if the
            regular file name is to be overridden (see documentation of
            appendFileNames in GMFFDoc\GMFFRunParms.txt).</dd><dd><code>theoremLabel</code> - the label of the theorem whose proof is being
            exported.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Confirmation message of the successful export showing the
         absolute path of the output file.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if the output operation fails.</dd></dl>
</li>
</ul>
<a name="writeExportFile(java.lang.String, java.lang.StringBuilder, boolean)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>writeExportFile</h4>
<pre>protected&nbsp;java.lang.String&nbsp;writeExportFile(java.lang.String&nbsp;exportFileName,
                               java.lang.StringBuilder&nbsp;exportBuffer,
                               boolean&nbsp;append)
                                    throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Writes the export text to the specified file and returns a String
 containing the absolute path of the output file.
 <p>
 Note that here is where the last of the Export Parms come into play,
 including the Export Directory and the Charset Encoding name. Export Type
 is used in error messages, just to be helpful.
 <p>
 The actual I/O operation is handled by <code>GMFFExportfile</code>.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exportFileName</code> - the output file, including file type.</dd><dd><code>exportBuffer</code> - the output text data.</dd><dd><code>append</code> - true if file is to be opened in "append mode", otherwise
            false.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String containing the absolute path of the export file.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if the output operation fails.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/GMFFExporterTypesetDefs.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/GMFFExporter.html" target="_top">Frames</a></li>
<li><a href="GMFFExporter.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
